(set-logic QF_BV)
(set-option :opt.priority box)
(set-option :model_validate true)
(set-option :model true)
(set-option :nlsat.check_lemmas false)
(set-option :nlsat.log_lemmas false)
(set-option :smt.phase_selection 4)
(set-option :smt.threads 1)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const bv_27-0 (_ BitVec 27))
(declare-const v15 Bool)
(declare-const bv_7-0 (_ BitVec 7))
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const bv_28-0 (_ BitVec 28))
(declare-const v21 Bool)
(declare-const bv_26-0 (_ BitVec 26))
(declare-const v22 Bool)
(declare-const bv_16-0 (_ BitVec 16))
(declare-const bv_16-1 (_ BitVec 16))
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const v26 Bool)
(declare-const v27 Bool)
(assert (or (and v11 v17 v2 v6)))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v25))
(assert (or v11 v26 v25))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) (and v11 v17 v2 v6) v11 v11 v26 v11 v11))
(assert (or v25))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2)))
(assert (or v25 v5 v6 v11 v26 v25))
(assert (or v6 v5 (and v11 v17 v2 v6) v6))
(assert (or v6))
(assert (or v11 v5 v26 (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v11))
(assert (or v25))
(assert (or v25))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2)))
(assert (or v25 (and v11 v17 v2 v6)))
(assert (or v25 v11 v6))
(assert (or v5 v25))
(assert (or v26))
(assert (or v6))
(assert (or v25 v25 v6 v6))
(assert (or v11))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v26))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2)))
(assert (or v11))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v6 v6))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v11))
(assert (or (and v11 v17 v2 v6) v11 v25 (and v11 v17 v2 v6) v26))
(assert (or v11 v26))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v25 v6))
(assert (or v26 v6 (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v11))
(assert (or v26 v6 v5 v6 v11 v6 v26))
(assert (or v25 v5 v11))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v6 v6 v6 v6))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v25 v25))
(assert (or (and v11 v17 v2 v6) (and v11 v17 v2 v6)))
(assert (or (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v11 v25))
(assert (or v26 v5 v25 v25 (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v11 v11 v11))
(assert (or v11 v26))
(assert (or (and v11 v17 v2 v6) v25 (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2)))
(assert (or v26))
(assert (or v5 v6 v6 (or v5 v9 v13 (bvult bv_27-0 bv_27-0) (distinct v11 v15 (bvult bv_27-0 bv_27-0)) v0 v2) v6 v25 v11 v26))
(minimize bv_7-0)
(maximize bv_16-0)
(minimize bv_26-0)
(minimize bv_27-0)
(maximize bv_28-0)
(check-sat)
(exit)
